optimization and formal methods

We present a machine-checked source containing 78 named real-arithmetic declarations that occur as local steps in standard analyses of stochastic gradient descent (SGD). This declaration count includes support identities, recovery variants, and direct restatements; it is not a count of novel or publication-credit theorems.